/*
 * HashMapClauseSetTest.cpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#include <gtest/gtest.h>

#include "bfr/ClauseSet.hpp"
#include "bfr/Clause.hpp"

namespace bfr { namespace test {

TEST(HashedClauseSet, insert_contains) {
    ClauseSet dnf(3);

    EXPECT_EQ(0, dnf.size());
    EXPECT_EQ("{}", dnf.asString());

    Clause *c1 = new Clause(1);
    c1->addSecure(new Literal(0));
    dnf.addSecure(c1);
    EXPECT_EQ("{{x0}}", dnf.asString());

    Clause *c2 = new Clause(2);
    c2->addSecure(new Literal(1, false));
    c2->addSecure(new Literal(2));
    dnf.add(c2);
    EXPECT_EQ(2, dnf.size());

    Clause *c2Other = new Clause(2);
    c2Other->addSecure(new Literal(1, false));
    c2Other->addSecure(new Literal(2));
    dnf.add(c2Other);
    EXPECT_EQ(2, dnf.size());

    Clause *empty = new Clause();
    EXPECT_TRUE(dnf.contains(c1));
    EXPECT_TRUE(dnf.contains(c2Other));
    EXPECT_FALSE(dnf.contains(empty));
    delete c2Other;
    delete empty;
}}
}

